COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 
C00025 ENDMK
C⊗;
 
to write unify(x,y) where x and y are sequences containing variables, constants
or functional terms. The mgu is returned if x and y are unifable; the mgu is 
either empty or a sequence of pairs (of substitutions), such that application
of the substitutions to x and y results in identical expressions; if x and y
are not unifiable the  atom LOSE is returned.


want unify as double  loop on x and y, with value returned in z.

(1)** V8    (note: V1-V8 displayed on scope as Vi:name with user commands to fondle)

procedure q(x;v);A

(2)** q:unify,x:x;y,v:z

procedure unify(x,y;z);A

(3)** A:V4              (iteration)

procedure unify(x,y;z);A;while S do B

(4)**S:¬empty[x]∧¬empty[y], B:V1(x,rest(x)),V1(y,rest(y))

procedure unify(x,y;z);A;while ¬empty[x]∧¬empty[y] do B;x←rest[x];y←rest[y];

(5)**A:null

procedure unify(x,y;z);while ¬empty[x]∧¬empty[y] do B;x←rest[x];y←rest[y];




Before going off to write {B} we should try to tighten up the
outer loops: namely there is no point to bother with {B} if z is LOSE.
So we wish to modify  the termination on "while" to exit if LOSE is
given to z as value.

(6)** (4):S+z≠LOSE
This results in:

procedure unify(x,y;z);
     while ¬empty[x]∧ ¬empty[y]∧¬z=LOSE do B;
     x←rest[x]; y← rest[y]}

(7)** B:V5		(conditional)

procedure unify(x,y;z);
     while ¬empty[x]∧ ¬empty[y]∧¬z=LOSE do 
      A;
      if Q then B else C;
     x←rest[x]; y← rest[y]}

(8)**A:V1(z1,*)

procedure unify(x,y;z);
     while ¬empty[x]∧ ¬empty[y]∧¬z=LOSE do 
      z1←E;
      if Q then B else C;
     x←rest[x]; y← rest[y]}

(9)**Q:issub(z1),B:V1(z;compose(z,z1));C:V1(z,LOSE)

procedure unify(x,y;z);
     while ¬empty[x]∧ ¬empty[y]∧¬z=LOSE do 
      z1←E;
      if issub(z1) then z←compose(z,z1) else z←LOSE;
     x←rest[x]; y← rest[y]}

(10)**E:unify1(subst(z;first(x));subst(z;first(y))

procedure unify(x,y;z);
     while ¬empty[x]∧ ¬empty[y]∧¬z=LOSE do 
      z1←unify1(subst(z;first(x));subst(z;first(y))
      if issub(z1) then z←compose(z,z1) else z←LOSE;
     x←rest[x]; y← rest[y]}


Now it seems reasonable to go after unify1[x;y] <= ... .


First here are commands which made program.
(1)** V8  
(2)** q:unify,x:x;y,v:z
(3)** A:V4  
(4)**S:¬empty[x]∧¬empty[y], B:V1(x,rest(x)),V1(y,rest(y))
(5)**A:null
(6)** (4):S+z≠LOSE
(7)** B:V5		
(8)**A:V1(z1,*)
(9)**Q:issub(z1),B:V1(z;compose(z,z1));C:V1(z,LOSE)
(10)**E:unify1(subst(z;first(x));subst(z;first(y))



notes: user's comments may  also go to transcript file.